Inference at * 
Iof proof for Lemma do-apply-p-filter:


  T:Type, P:(T), f:(x:T. Dec(P(x))), x:T.
  (can-apply(p-filter(f);x))  (do-apply(p-filter(f);x) = x) 

latex

 by (((if (((first_nat 4:n)) = 0) then (Repeat (((D (0)) 
CollapseTHENA (Auto))
Co)) else (RepeatFor (first_nat 4:n) (((D (0)) 
CollapseTHENA (Auto)))))) 
CollapseTHEN (
CoRepUR ``can-apply do-apply p-filter`` ( 0))) 

latex

Co1: 

Co1: 1. T : Type
Co1: 2. P : T
Co1: 3. f : x:T. Dec(P(x))
Co1: 4. x : T
Co1:   (isl(case f(x) of inl(p) => inl x  | inr(p) => inr p ))
Co1:    (outl(case f(x) of inl(p) => inl x  | inr(p) => inr p ) = x)
Co.

Definitions	Type, , Dec(P), x(s), f(a), t  T, x:A. B(x), P  Q, s = t, x:AB(x), can-apply(f;x), p-filter(f), do-apply(f;x), b
Lemmas	decidable wf